\label{sec:dsltrans}


\begin{definition}{Match Function}
\label{def:match_function}

Let $m\in MAM^{s}_{t}$ be a model and $tr\in TR^{s}_{t}$ be a transformation
rule. The $match : MAM^{s}_{t}\times TR^{s}_{t}\rightarrow
\mathcal{P}(TR^{s}_{t})$ is defined as follows: $$match_{tr}(m)=remove\big(\big\{g\;|\;
g\lhd m \land g \cong strip(tr)\big\}\big)$$

Due to the fact that the $\cong$ relation is based on the notion of graph
isomorphism, permutations of the same match result may exist in the
$\big\{g\;|\; g\lhd m \land g \cong strip(tr)\big\}$ set. The --- undefined ---
$remove:\mathcal{P}(TR^{s}_{t})\rightarrow \mathcal{P}(TR^{s}_{t})$ function is such that
it removes such undesired permutations.

%The $strip:TR^{s}_{t}\rightarrow TR^{s}_{t}$ function is such that
%$$strip(\big\langle V,E,T,\langle V_m,E_m,T_m,s\rangle,\langle V_a,E_a,T_a,t\rangle,Bl,Il\big\rangle) = \big\langle V',E',T,\langle V_m,E_m,T_m\rangle,\langle V'_a,E'_a,T_a\rangle,Bl,Il\big\rangle$$
%\begin{center}
%where $(v'\in V'_a\Rightarrow v\rightarrow v'\in Bl)\;\land\;(v\rightarrow v'\in E'_a\Rightarrow (v\rightarrow v'\in E_m \land \{v,v'\}\subseteq V'_a))$
%\end{center}
\end{definition}

\begin{definition}{Apply Function}
\label{def:apply_function}

Let $m\in MAM^{s}_{t}$ be a match-apply model and $tr\in TR^{s}_{t}$ a
transformation. The $apply : MAM^{s}_{t}\times TR^{s}_{t}\rightarrow MAM^{s}_{t}$
is defined as follows: 

$$apply_{tr}(m)=\bigsqcup_{g\in match_{tr}(m)}back(g\sqcup g_{\Delta})$$

\begin{center}
where $g_{\Delta}$ is such that $g \sqcup g_{\Delta}\cong tr$\\
\end{center}

The freshly created vertices of $g_\Delta$ in the flattened $apply_{tr}(m)$ set are disjoint. 
\end{definition}

 Definitions~\ref{def:match_function} and~\ref{def:apply_function} are
 complementary: the former gathers all subgraphs of a match-apply graph which
 match a transformation rule; the latter builds the new instances which are
 created by applying that transformation rule as many times as the number of
 subgraphs found by the $match$ function. The $strip$ function is used to
 enable matching over backward links but not elements to be created by the
 transformation rule. The $back$ function connects all newly created vertices
 to the elements of the source model that originated them.

%\begin{definition}{Transformation}

%Let $g\in TG$ be a typed graph. The graph transform function $transform : TR\times TG\rightarrow TG$ is recursively defined as:
%\begin{gather*}
%  transform_{(m,a)}(g) =
%  \begin{cases}
%    g  & \text{if } match_{m}(g)=\emptyset \\
%    instance(a)\cup transform_{(m,a)}(g') &\text{if } match_{m}(g)\neq \emptyset
%  \end{cases}
%\end{gather*}
%$$\text{where } g'=mark_{(m)}(g)$$
%\end{definition}

%\subsection{Transformation Semantics}
%\begin{definition} {Layer Semantics}

%Let $l\in Layer$ be a layer and $\{m,m'\} \in MAM^{s}_{t}$ be a match
%$$\frac{}
%{m,\emptyset \stackrel{layerstep}{\rightarrow}m}$$
%$$\frac{tr\in layer,\; transform_{tr}(m) = m''\; m'',layer\backslash\left\{tr\right\} \xrightarrow{layerstep}	 m'}{m,layer \xrightarrow{layerstep} m'}$$
%\end{definition}

\begin{definition} {Layer Step Semantics}
\label{def:layer_step_semantics}

Let $l\in Layer^{s}_{t}$ be a Layer. The \emph{layer step relation} $
LStep_{l}\subseteq MAM^{s}_{t}\times \mathcal{P}(TR^{s}_{t})\times
MAM^{s}_{t}$ (noted $\stackrel{layerstep}{\rightarrow}$) is defined as follows:

$$\frac{}
{\langle m,m',\emptyset\rangle \xrightarrow{layerstep}m \sqcup m'}$$

$$\frac{\begin{array}{ll}& tr\in l,\; apply_{tr}(m) = m''',\\
&\langle m,m''\sqcup m''',l\backslash \{tr\}\rangle \xrightarrow{layerstep} m'
\end{array}}
{\langle m,m'',l\rangle \xrightarrow{layerstep} m'}$$

\begin{center}
where $\{m,m',m''\} \subseteq MAM^{s}_{t}$ are match-apply models.
\end{center}

The freshly created vertices in $m'''$ are disjoint from those in $m''$.

\end{definition}

For each layer we go through all the transformation rules and build for each
one of them the set of new instances created by their application. These
instances are built using the $apply$ function in the second rule of
definition~\ref{def:layer_step_semantics}. The new instance results
of the $apply$ function for each transformation rule are accumulated until all
transformation rules are treated. Then, the first rule of
definition~\ref{def:layer_step_semantics} will merge all the new
instances with the starting match-apply model. The merge is performed by uniting
(using the non-disjoint $\sqcup$ union) match-apply graphs including the new instances with
the starting match-apply model. 

%Notice that this is only possible because the $\sqcup$ union is not disjoint.

\begin{definition} {Transformation Step Semantics}
\label{def:transformation_step_semantics}


Let $tf=[l::R]\in Transformation^{s}_{t}$ be a Transformation, where $l\in
Layer^{s}_{t}$ is a Layer and $R$ a list. The \emph{transformation step relation}
$TRStep_{tf}\subseteq MAM^{s}_{t}\times TR^{s}_{t}\times
MAM^{s}_{t}$ (noted $\stackrel{trstep}{\rightarrow}$) is defined as follows:
$$\frac{}{\langle m,[]\rangle \xrightarrow{trstep}m}$$.

$$\frac{\big\langle m,\langle\emptyset,\emptyset,\emptyset, \emptyset,
\emptyset, \emptyset, \emptyset \rangle,l\big\rangle \xrightarrow{layerstep} m'',\; \langle
m'',R\rangle \xrightarrow{trstep} m'}{\langle m,tf\rangle
\xrightarrow{trstep} m'}$$

\begin{center}
where $\{m,m',m''\} \subseteq MAM^{s}_{t}$ are match-apply models.  An element
$ti\in TRStep_{tr}$ is called a \emph{transformation instance} of
transformation ${tr}$.
\end{center}

\end{definition}

A model transformation is a sequential application of
transformation layers to a match-apply model containing the source
model and an empty apply model. The transformation output is the apply
part of the resulting match-apply model.

\begin{definition} {Model Transformation}
\label{def:modeltransformation}

Let $m_s \in MODEL^{s}$ and $m_t \in MODEL^{t}$ be models and \\$tf\in
Transformation^{s}_{t}$ be a transformation. A model transformation
$Transf_{tf}\subseteq MODEL^{s}\times Transformation^{s}_{t}
\times MODEL^{t}$ (noted $\stackrel{transf}{\rightarrow}$) is defined as
follows:
\begin{multline*}
m_s,tf\xrightarrow{transf} m_t \Leftrightarrow
\langle V,E,\tau_{V},\tau_{E},m_s,\emptyset, \emptyset\rangle, unfold(tf)
\xrightarrow{trstep} \langle V,E,\tau_{V},\tau_{E},m_s,m_t, Bl\rangle
\end{multline*}
\end{definition}

We now prove two important properties about DSLTrans' transformations.

\begin{proposition}{Confluence}

Every model transformation is confluent regarding typed graph equivalence.
\end{proposition}
\begin{proof}
(Sketch) We want to prove that for every model transformation $tf\in
Transformation^{s}_{t}$ having as input a model $m_s \in MODEL^{s}$, if
$m_s,tf\xrightarrow{transf} m_t$ and $m_s,tf\xrightarrow{transf} m'_t$ then
$m_t\cong m'_t$. Note that we only have to prove typed graph equivalence between
$m_t$ and $m'_t$ because the identifiers of the objects produced by a model
transformation are irrelevant.
If we assume $\neg(m_t\cong m'_t)$ then this should happen because of
non-determinism points in the rules defining the semantics of a transformation:
 1) in definition~\ref{def:apply_function} $g_{\Delta}$ is non-deterministic up
 to typed graph equivalence, which does not contradict the proposition; 2) in
 definition~\ref{def:layer_step_semantics} transformation rule $tf$ is chosen
 non-deterministically from layer $l$. Thus, the order in which the
 transformation rules are treated is non-deterministic. However, the increments
 to the transformation by each rule of a layer are united using $\sqcup$, which
 is commutative and thus renders the transformation result of each layer
 deterministic.
Since there are no other possibilities of non-determinism points in the
semantics of a transformation, $\neg(m_t\cong m'_t)$ provokes a contradiction
and thus the proposition is proved.
\end{proof}

\begin{proposition}{Termination}

Every model transformation terminates.
\end{proposition}
\begin{proof}
(Sketch) Let us assume that there is a transformation which does not terminate.
In order for this to happen there must exist a section of the semantics of that
transformation which induces an algorithm with an infinite amount of steps. We
identify three points of a transformation's semantics where this can happen: 1)
if definition~\ref{def:transformation_step_semantics} induces an infinite amount
of steps. The only possibility for this to happen is if the transformation has
an infinite amount of layers, which is a contradiction with
definition~\ref{def:layer_transformation}; 2) if
definition~\ref{def:layer_step_semantics} induces an infinite amount of steps.
The only possibility for this to happen is if a layer has an infinite amount of
transformation rules, which is a contradiction with
definition~\ref{def:layer_transformation}; 3) if the result of the
$match_{tf}(m)$ function in
 definition~\ref{def:match_function} is an infinite set of match-apply graphs.
 The match-apply graph $m$ is by definition finite, thus the number of
 isomorphic subgraphs of $m$ is infinite only if the transitive closure of
 containment edges of $m$ is infinite. The only possibility for this to happen
 is if the graph induced by the containment edges of $m$ has cycles, which
 contradicts definition~\ref{def:typed_graph}.
Since there are no more points in the semantics of a transformation that can
induce an infinite amount of steps, the proposition is
proved.
\end{proof}
